宅在家里最适合看的编程，C++、Java还是……沈从文？

在家办公的假期，省去通勤的时间，买本“编程”来看？

选择C++，Java，Python？

亦或者，沈从文？

当然了，《边城》也许确实是个在寂寞无聊时陪伴你的不错选择，毕竟它是排名仅次于鲁迅《呐喊》的20世纪中文小说。不过鉴于最近很多人在朋友圈以及各大网络平台呐喊到喉咙沙哑，不妨换个口味学习下这样的编程。

它不是C++，不是Java，也不是Python，而是一款用代码就可以保证安全的编程语言——DeepSEA。学习它的理由只需这一点，那就是无论当下这个特殊时期还是平日里没有疫情循环往复的周一到周日，安全都是每个行业永恒的重心。

安全，各行各业都需要将这个词铭记在心。相信很多人都知道这点，只是最近才逐渐意识到它的重要性。互联网，特别是区块链领域，更是如此。区块链行业，就如同城市中新兴的最高耸的玻璃大厦，而安全防护就如同雷电交加的夜晚中大厦顶尖上的那颗避雷针。把各种编程语言运用的再熟练的程序员，也依然不能百分百保证结构没有漏洞。于是我们便需要这样一种编程语言，来确保智能合约的安全性。

DeepSEA：用于编写可验证智能合约的新语言。它是一种新型函数式编程语言，它可通过代码形式充分保证智能合约的安全性。 

DeepSEA是一种编程语言，用它编写的程序可以处理极其复杂的代码，同时保证编码人员每项操作的安全性。在对Coq系统进行完整的形式化验证时，这一语言便可以充分发挥其作用。

CertiK提供的形式化验证可从数学层面验证代码是否可按预期工作，并精密计算出所有可能出现的发展。作为智能合约和区块链形式化验证领域的领先者，CertiK还发现，形式化验证是及时发现代码内涵漏洞并规避漏洞的唯一方法，但是这并不能保证编写的代码从一开始就是正确的。

造成这种情况的一部分原因是因为缺乏编程语言的支持。现有的语言（例如C语言或OCaml或Solidity）都无法与验证工具很好地结合在一起，且需要大量时间来创建和验证人工证明。不一样的是，DeepSEA语言提供了一种方法，这种方法通过Coq证明助手就能以可扩展和自动化方式对智能合约进行形式化验证。

开发人员往往花费大量时间在诸如Coq之类的交互式证明助手中编写证明，此时，DeepSEA可有效帮助他们减少繁杂工作，将复杂系统结构简化为独立模块，从而使系统的各部分都能通过安全验证。

在设计语言时，我们提出了四个创建原则，这些原则综合了其他几种编程语言的最佳功能：

• 公式推理：每个DeepSEA术语都将被转换为相应的功能规范，可以在Coq证明助手中进行推理。

• 分层规范：DeepSEA可通过抽象层管理证明，这些抽象层提供了程序的高级视图。编译器证明原始字节码实现的行为符合设计预期，而程序员只需要查看高级视图即可。

• 分类和组合：每个DeepSEA层均由在另一层之上构建的对象组成，这些层可以一次性证明正确性。

• 抽象优化功能：DeepSEA通过用户友好型操作来验证大型系统。该过程由一系列证明构成，这些证明可以验证链接程序是否符合规范。

区块链生态系统必须要建立在信任的基础上。有些人认为区块链值得信赖的原因在于共识协议，但由于某些可能产生的程序编写错误及恶意攻击，代码仍不可完全保证其安全性。

例如，如果智能合约中的某个特定功能溢出了或者是功能实现不符合设计规范，既会产生漏洞。

寻求对于程序的信任对于区块链行业很重要，因为智能合约一旦部署就无法撤消，一旦产生漏洞，日后非常容易被黑客利用。

形式化验证是检验代码无漏洞并对代码的数学事实进行验证的唯一可靠方法。证明程序正确处理了所有可能的输入值，便可以从数学层面确保代码按预期工作。在所有应用形式验证的情况下，DeepSEA可帮助开发人员证明任意数量的复杂合约。

合约的复杂度不一，形式化验证也是如此。现有的自动工具可以很好地处理通证等简易合约，而要验证诸如表决方案或跨链交互之类的复杂合约，我们就需要其他工具来处理相关的复杂规范和证明。

处理复杂合约时，像Coq这样的交互式证明助手就能大放异彩。通过集成智能合约和Coq，我们可以将形式化验证应用于最具挑战性的任务，对系统进行端到端的全面验证。

如今几乎所有合约均以编程语言编写，但这些编程语言在设计时并未考虑应用到形式化验证里。即使将它们与形式化验证系统结合在一起，它们也只能处理简单的事项。

内置的Solidity SMT就是一个很好的例子。SMT求解器允许程序员使用假定为真的条件注释函数，编写应保留的证明，并使编译器自动对其进行验证。

但是，以上功能仅能在固定的数字和数组中发挥作用，而且只能在特定的单个函数调用期间影响程序状态。也就是说，求解器只能证明某项判断，而不能证明程序中的其他内容是否正确。同时，用户必须相信编译器本身是正确的。但是编译的正确与否无法保证。

其他验证系统（例如K框架）通过使用EVM规范以及允许程序员进行人工审计（例如，提供循环不变式）来消除代码的一些问题。但是，这些验证系统缺乏抽象性，只关注固定化单次运行的属性。

为了能够验证复杂合约的属性，CertiK预备使用像Coq或Isabelle这样的交互式证明助手。交互式证明助手一般具有内置的编程语言，但它们是通过使用自动内存收集器的功能性编程语言进行编译的。

在区块链行业中，自动内存收集器不仅会使智能合约的编译进程效率低下，还会花费巨额成本，整个进程所耗燃料甚高。因此，Coq的内置语言不能直接用于以太坊。幸运的是，DeepSEA编译器能够通过生成高效的可执行代码和可加载到Coq中的形式化模型来弥补这一不足。

DeepSEA是一种灵活且兼容的语言，可以使用Coq创建具有高度抽象和推理功能的直观设计。CertiK相信，借助新一代技术，区块链的安全性将能够得到保证。DeepSEA为保护代码提供了有效的解决方案。

目前，DeepSEA已于CertiK官网上线：https://certik.org/research/deepsea/。日后，CertiK将会发布更多有关DeepSEA的文章以及消息，敬请关注！

了解更多

General Information: [e-mail]

Audit & Partnerships: [e-mail]

Website: certik.org

Twitter: @certik.org

Telegram: t.me/certik.org

Medium:medium.com/certik

币乎：bihu.com/people/1093109

往期回顾

请点击“阅读原文”访问CertiK官方网站